$\vdash$  $\forall$$A$:Type, $L$:($A$ List), $n$:$\mathbb{N}$. ($n$ $\leq$ $\parallel$$L$$\parallel$) $\Rightarrow$ ($\parallel$lastn($n$;$L$)$\parallel$ = $n$)